Celestin Apprentice 7/Apprentice-Release7.iso/Environments/Small Eiffel 0.4.8/lib_std/comparable.e

Text File | 1997-04-13 | 3KB | 123 lines

-- Part of SmallEiffel -- Read DISCLAIMER file -- Copyright (C)
-- Dominique COLNET and Suzanne COLLIN -- [e-mail]
--
deferred class COMPARABLE
   --
   -- All class handling COMPARABLE object with a total order relation
   -- should inherit from this class.
   --

inherit ANY redefine is_equal end;

feature

   infix "<" (other: like Current): BOOLEAN is
     -- Is 'Current' strictly less than 'other'?
      require
     other_exists: other /= Void
      deferred
      ensure
     asymmetric: Result implies not (other < Current);
      end;

   infix "<=" (other: like Current): BOOLEAN is
     -- Is 'Current' less or equal 'other'?
      require
     other_exists: other /= Void
      do
     Result := not (Current > other)
      ensure
     definition: Result = (Current < other) or is_equal(other);
      end;

   infix ">" (other: like Current): BOOLEAN is
     -- Is 'Current' strictly greater than 'other'?
      require
     other_exists: other /= Void
      do
     Result := (other < Current)
      ensure
     definition: Result = (other < Current)
      end;

   infix ">=" (other: like Current): BOOLEAN is
     -- Is 'Current' greater or equal than 'other'?
      require
     other_exists: other /= Void
      do
     Result := not (Current < other)
      ensure
     definition: Result = (other <= Current)
      end;

   in_range(lower, upper: like Current): BOOLEAN is
         -- Return true if Current is in range [`lower'..`upper']
      do
     Result := (Current >= lower) and then (Current <= upper)
      ensure
     Result = (Current >= lower and Current <= upper)
      end;

   is_equal(other: like Current): BOOLEAN is
      do
     if Current < other then
     elseif other < Current then
     else
        Result := true;
     end;
      ensure then
     trichotomy: Result = (not (Current < other)
                   and not (other < Current));
      end;

   compare(other: like Current): INTEGER is
     -- Compare 'Current' with 'other'.
     -- '<' <==> Result < 0
     -- '>' <==> Result > 0
     -- Otherwise Result = 0.
      require
     other /= Void
      do
     if Current < other then
        Result := -1
     elseif other < Current then
        Result := 1
     end
      ensure
     (Result < 0) = (Current < other);
     (Result = 0) = not (Current < other or Current > other);
     (Result > 0) = (Current > other)
      end;

   min(other: like Current): like Current is
     -- Minimum of 'Current' and 'other'.
      require
     other /= Void
      do
     if Current < other then
        Result := Current
     else
        Result := other
     end;
      ensure
     Result <= Current and then Result <= other;
     compare(Result) = 0 or else other.compare(Result) = 0
      end;

   max(other: like Current): like Current is
     -- Maximum of 'Current' and 'other'.
      require
     other /= Void
      do
     if other < Current then
        Result := Current;
     else
        Result := other;
     end;
      ensure
     Result >= Current and then Result >= other;
     compare(Result) = 0 or else other.compare(Result) = 0
      end;

end -- COMPARABLE